\begin{tabbing}
fischer\=\{\=\$x:ut2,\+\+
\\[0ex]\$try:ut2,
\\[0ex]\$taken:ut2,
\\[0ex]\$contending:ut2,
\\[0ex]\$free:ut2,
\\[0ex]\$mine:ut2,
\\[0ex]\$wanted:ut2,
\\[0ex]\$z:ut2\}
\-\\[0ex](${\it es}$; $L$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$e$:es{-}E(${\it es}$). \+
\\[0ex](loc($e$) $\in$ $L$)
\\[0ex]$\Rightarrow$ \=(es{-}dtype(${\it es}$; loc($e$); mkid\{\$x:ut2\}; Id)\+
\\[0ex]c$\wedge$ \=(\=((es{-}after(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$free:ut2\})\+\+
\\[0ex]$\vee$ (es{-}after(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$taken:ut2\})
\\[0ex]$\vee$ (es{-}after(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$mine:ut2\})
\\[0ex]$\vee$ (es{-}after(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$try:ut2\})
\\[0ex]$\vee$ (es{-}after(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$contending:ut2\}))
\-\\[0ex]$\wedge$ (es{-}initially(${\it es}$; loc($e$); mkid\{\$x:ut2\}) = mkid\{\$free:ut2\})
\\[0ex]$\wedge$ \=(@$e$(mkid\{\$x:ut2\}$\rightarrow$mkid\{\$try:ut2\})\+
\\[0ex]$\Rightarrow$ \=(((es{-}when(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$free:ut2\})\+
\\[0ex]$\vee$ (es{-}when(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$contending:ut2\}))
\\[0ex]$\wedge$ l\_all(\=$L$;\+
\\[0ex]Id;
\\[0ex]$i$.(($\neg$($i$ = loc($e$)))
\\[0ex]$\Rightarrow$ \=($e$ sends on $<$loc($e$)\+
\\[0ex], $i$
\\[0ex], mkid\{\$z:ut2\}$>$ with tag mkid\{\$wanted:ut2\})))))
\-\-\-\-\\[0ex]$\wedge$ \=(@$e$(mkid\{\$x:ut2\}$\rightarrow$mkid\{\$mine:ut2\})\+
\\[0ex]$\Rightarrow$ (es{-}when(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$try:ut2\}))
\-\\[0ex]$\wedge$ \=(@$e$(mkid\{\$x:ut2\}$\rightarrow$mkid\{\$free:ut2\})\+
\\[0ex]$\Leftarrow\!\Rightarrow$ \=(((es{-}when(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$taken:ut2\})\+
\\[0ex]$\wedge$ \=(($\uparrow$es{-}isrcv(${\it es}$; $e$))\+
\\[0ex]c$\wedge$ \=((es{-}tag(${\it es}$; $e$) = mkid\{\$free:ut2\})\+
\\[0ex]$\wedge$ ($\exists$\=$i$:Id\+
\\[0ex](($i$ $\in$ $L$)
\\[0ex]$\wedge$ ($\neg$($i$ = loc($e$)))
\\[0ex]$\wedge$ (es{-}lnk(${\it es}$; $e$) = $<$$i$, loc($e$), mkid\{\$z:ut2\}$>$))))))
\-\-\-\\[0ex]$\vee$ \=((es{-}when(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$mine:ut2\})\+
\\[0ex]$\wedge$ l\_all(\=$L$;\+
\\[0ex]Id;
\\[0ex]$i$.(($\neg$($i$ = loc($e$)))
\\[0ex]$\Rightarrow$ \=($e$ sends on $<$loc($e$)\+
\\[0ex], $i$
\\[0ex], mkid\{\$z:ut2\}$>$ with tag mkid\{\$free:ut2\}))))))
\-\-\-\-\-\\[0ex]$\wedge$ \=(@$e$(mkid\{\$x:ut2\}$\rightarrow$mkid\{\$contending:ut2\})\+
\\[0ex]$\Leftarrow\!\Rightarrow$ \=((es{-}when(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$try:ut2\})\+
\\[0ex]$\wedge$ \=(($\uparrow$es{-}isrcv(${\it es}$; $e$))\+
\\[0ex]c$\wedge$ \=((es{-}tag(${\it es}$; $e$) = mkid\{\$wanted:ut2\})\+
\\[0ex]$\wedge$ ($\exists$\=$i$:Id\+
\\[0ex](($i$ $\in$ $L$)
\\[0ex]$\wedge$ ($\neg$($i$ = loc($e$)))
\\[0ex]$\wedge$ (es{-}lnk(${\it es}$; $e$) = $<$$i$, loc($e$), mkid\{\$z:ut2\}$>$)))))))
\-\-\-\-\-\\[0ex]$\wedge$ \=(@$e$(mkid\{\$x:ut2\}$\rightarrow$mkid\{\$taken:ut2\})\+
\\[0ex]$\Rightarrow$ \=(((es{-}when(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$contending:ut2\})\+
\\[0ex]$\vee$ (es{-}when(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$free:ut2\}))
\\[0ex]$\wedge$ \=(($\uparrow$es{-}isrcv(${\it es}$; $e$))\+
\\[0ex]c$\wedge$ \=((es{-}tag(${\it es}$; $e$) = mkid\{\$wanted:ut2\})\+
\\[0ex]$\wedge$ ($\exists$\=$i$:Id\+
\\[0ex](($i$ $\in$ $L$)
\\[0ex]$\wedge$ ($\neg$($i$ = loc($e$)))
\\[0ex]$\wedge$ (es{-}lnk(${\it es}$; $e$) = $<$$i$, loc($e$), mkid\{\$z:ut2\}$>$)))))))
\-\-\-\-\-\\[0ex]$\wedge$ \=(($\uparrow$es{-}isrcv(${\it es}$; $e$))\+
\\[0ex]$\Rightarrow$ (es{-}tag(${\it es}$; $e$) = mkid\{\$free:ut2\})
\\[0ex]$\Rightarrow$ ($\exists$\=$i$:Id\+
\\[0ex](($i$ $\in$ $L$)
\\[0ex]$\wedge$ ($\neg$($i$ = loc($e$)))
\\[0ex]$\wedge$ (es{-}lnk(${\it es}$; $e$) = $<$$i$, loc($e$), mkid\{\$z:ut2\}$>$)))
\-\\[0ex]$\Rightarrow$ \=(subtype\_rel(es{-}vartype(${\it es}$; loc(es{-}sender(${\it es}$; $e$)); mkid\{\$x:ut2\}); Id)\+
\\[0ex]c$\wedge$ \=(@es{-}sender(${\it es}$; $e$)(mkid\{\$x:ut2\}$\rightarrow$mkid\{\$free:ut2\})\+
\\[0ex]$\wedge$ (es{-}when(${\it es}$; mkid\{\$x:ut2\}; es{-}sender(${\it es}$; $e$)) = mkid\{\$mine:ut2\}))))
\-\-\-\\[0ex]$\wedge$ \=(($\uparrow$es{-}isrcv(${\it es}$; $e$))\+
\\[0ex]$\Rightarrow$ (es{-}tag(${\it es}$; $e$) = mkid\{\$wanted:ut2\})
\\[0ex]$\Rightarrow$ ($\exists$\=$i$:Id\+
\\[0ex](($i$ $\in$ $L$)
\\[0ex]$\wedge$ ($\neg$($i$ = loc($e$)))
\\[0ex]$\wedge$ (es{-}lnk(${\it es}$; $e$) = $<$$i$, loc($e$), mkid\{\$z:ut2\}$>$)))
\-\\[0ex]$\Rightarrow$ \=(subtype\_rel(es{-}vartype(${\it es}$; loc(es{-}sender(${\it es}$; $e$)); mkid\{\$x:ut2\}); Id)\+
\\[0ex]c$\wedge$ @es{-}sender(${\it es}$; $e$)(mkid\{\$x:ut2\}$\rightarrow$mkid\{\$try:ut2\})))))
\-\-\-\-\-
\end{tabbing}